T:Type, as:(T List), f,g:(T).
((priority-select(f; g; as) = (inl tt )  (?))
 (i:int_seg(0; ||as||). (((f(as[i])))  (j:int_seg(0; i). ((g(as[j])))))))
 ((priority-select(f; g; as) = (inl ff )  (?))
  (i:int_seg(0; ||as||). (((g(as[i])))  (j:int_seg(0; (i + 1)). ((f(as[j])))))))
 ((priority-select(f; g; as) = (inr  )  (?))
  (i:int_seg(0; ||as||). (((f(as[i]))))  (((g(as[i])))))) 

latex

Definitions

b, t  T, , Unit, int_seg(i; j), A, x:A. B(x), P  Q, x:A. B(x), P  Q, priority-select(f; g; as), , tl(l), i <z j, b, i z j, if b then t else f fi , Y, nth_tl(n;as), hd(l), l[i], A  B, lelt(i; j; k), ff, prop{i:l}, P  Q, False, tt, ||as||, P  Q, P  Q, decidable(P), x. t(x), isl(x), list_accum(x,a.f(x;a); y; l), ge(i; j), True, guard(T), sq_type(T), x,y. t(x;y), T

Lemmas

squash wf, true wf, select cons tl, le wf, iff functionality wrt iff, list accum wf, isl wf, ifthenelse wf, decidable int equal, length cons, bool sq, assert elim, int seg properties, length wf1, non neg length, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, decidable ex int seg, decidable cand, decidable all int seg, decidable not, decidable assert, int seg wf, not wf, assert wf, select wf, length wf2, btrue wf, it wf, bfalse wf, unit wf, bool wf